A, B:(IdMsgA). interface-compatible(A;B)  Prop 

latex

Definitions	interface-compatible(A;B), IdLnk, P & Q, P  Q, interface-link(A;B;l;tg), M.dout(l,tg), source(l), M.din(l,tg), destination(l), x:A. B(x), Id, t  T, MsgA
Lemmas	msga wf, Id wf, ldst wf, ma-din wf, lsrc wf, ma-dout wf, subtype rel wf, interface-link wf, IdLnk wf